;;;============================================================
;;;
;;; Subject: Invariant help Kenzo
;;;
;;;------------------------------------------------------------
;;;
;;; Jónathan Heras Vicente
;;; Date: 04-10-09
;;;
;;;============================================================

#| Certification code:

(certify-book "help-invariant" 0 nil)

|#


(in-package "ACL2")

(include-book "1dlop-dgop-do-cmp-d-ls-d-do")

;;(include-book "generic-kenzo-properties-imp2")

(defthm a-lemma1
  (implies (and (cmp-d-ls-d-do i ls)
		(dgl-p ls)
		(natp i)
		(<= i (car ls)))
	   (<= (cmp-d-ls-d-do i ls)
	      i))
:hints (("Goal" :induct (cmp-d-ls-d-do i ls))))
		

(defthm a-lemma2
  (implies (and (cmp-d-ls-d-do i ls)
		(dgl-p ls)
		(natp i)
		(<= i (car ls)))
	   (<= (cmp-d-ls-d-do i ls)
	      (- (car ls) (len ls))))
:hints (("Goal" :induct (cmp-d-ls-d-do i ls))))



(defun expt=>len-equal-schema (q)
  (if (or (not (natp q)) (not (> q 0)))
      nil
    (expt=>len-equal-schema (- q 1))))

(in-theory (enable ash-to-floor))

(defthm expt=>len-equal
  (implies (and (natp q)
		(> q 0))
	   (equal (len (dgn->dgb (expt 2 q))) (+ q 1)))
:hints (("Goal" 
	 :induct (expt=>len-equal-schema q))))



(defthm expt=>len-equal-case-0
  (implies (and (eql q 0)
		)
	   (equal (len (dgn->dgb (expt 2 q))) (+ q 1)))
)

(defthm expt=>len-equal-all
  (implies (natp q)
	   (equal (len (dgn->dgb (expt 2 q))) (+ q 1)))
:hints (("Goal" :do-not-induct t
	 :use ((:instance expt=>len-equal-case-0)
	       (:instance expt=>len-equal)))))

(defthm expt=>len-equal-bis
  (implies (and (natp q)
		(natp dgop)
		(> q 0)
		(= dgop (expt 2 (- q 1))))
	   (= (len (dgn->dgb dgop)) q))
)


(defthm expt=>len-equal-dgop-1
  (implies (and (natp q)
		(> q 0))
	   (equal (len (dgn->dgb (1- (expt 2 q)))) q))
:hints (("Goal" :INDUCT (EXPT=>LEN-EQUAL-SCHEMA Q))
	
	))


(defun len-dgn->dgb-a<=b-schema (a b)
  (if (or (not (natp a)) (not (natp b)) (not (<= a b))
	  (not (> b 0)) (not (> a 0)))
      nil
    (if (zp b)
	t
      (len-dgn->dgb-a<=b-schema (ash a -1) (ash b -1)))))


(defthm len-dgn->dgb-a<=b
  (implies (and (natp a)
		(natp b)
		(> b 0)
		(> a 0)
		(<= a b))
	   (<= (len (dgn->dgb a))
	       (len (dgn->dgb b))))
:hints (("Goal" :induct (len-dgn->dgb-a<=b-schema a b))))



(defthm expt=>len-equal-<
  (implies (and (natp q)
		(natp dgop)
		(> q 0)
		(<= dgop (1- (expt 2 q))))
	   (<= (len (dgn->dgb dgop)) q))
:hints (("Goal" :do-not-induct t
	 :use ((:instance len-dgn->dgb-a<=b
			  (a dgop)
			  (b (1- (expt 2 q))))
	       (:instance expt=>len-equal-dgop-1)
			  ))))

(defthm expt=>len-equal-<2
  (implies (and (natp q)
		(natp dgop)
		(= q 0)
		(<= dgop (1- (expt 2 q))))
	   (<= (len (dgn->dgb dgop)) q))
)


(defthm expt=>len-equal-<3
  (implies (and (natp q)
		(natp dgop)
		(<= dgop (1- (expt 2 q))))
	   (<= (len (dgn->dgb dgop)) q))
:hints (("Goal" :do-not-induct t
	   :use ((:instance expt=>len-equal-<)
		 (:instance expt=>len-equal-<2)
	   ))))

(defun len=>expt<-schema (dgop q)
  (if (or (not (natp q)) (not (> q 0)) (not (dgb-p dgop))
	       (not (<= (len dgop) q)))
      nil
    (if (consp dgop)
	(len=>expt<-schema (cdr dgop) (- q 1))
      t)))


(defthm consp-len
  (implies (consp a)
	   (< 0 (len a))))


(defthm consp-len-not
  (implies (consp a)
	   (not (equal (len a) 0)))
  )


(defthm ash-expt-1
  (implies (natp q)
	   (eql (ash (- (expt 2 q) 1) 1)
		(- (expt 2 (+ q 1)) 2))))

(defthm len-dgop<=1-implies-dgb->dgn-aux
  (implies (and (consp a)
		(dgb-p a)
		(<= (len a) 1))
	   (equal a '(1)))
:rule-classes nil)

(defthm len-dgop<=1-implies-dgb->dgn
  (implies (and (consp a)
		(dgb-p a)
		(<= (len a) 1))
	   (<= (* 2 (dgb->dgn a)) 3))
:hints (("Goal" :do-not-induct t
	 :use ((:instance len-dgop<=1-implies-dgb->dgn-aux)))))

(defthm len-dgop<=1-implies-dgb->dgn2
  (implies (and (consp a)
		(dgb-p a)
		(<= (len a) 1))
	   (<= (dgb->dgn a) 1))
:hints (("Goal" :do-not-induct t
	 :use ((:instance len-dgop<=1-implies-dgb->dgn-aux)))))



(defthm len=>expt<-aux1-1
  (implies (and (natp q)
		(> q 1)
		(natp a)
		(<= (+ 1 a) (expt 2 (1- q))))
	   (<= a (- (expt 2 (1- q)) 1))))



(defthm len=>expt<-aux1-2
  (implies (and (natp q)
		(> q 1)
		)
	   (equal (* 2 (expt 2 (1- q)))
		  (expt 2 q)
	   )))



(defthm len=>expt<-aux1-3
  (implies (and (natp q)
		(> q 1)
		(natp a)
		(<= (+ 1 a) (expt 2 (1- q))))
	   (<= (+ 1 (* 2 a)) (+ 1 (* 2 (- (expt 2 (1- q)) 1)))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance len=>expt<-aux1-1)))))



(defthm len=>expt<-aux1
  (implies (and (natp q)
		(> q 1)
		(natp a)
		(<= (+ 1 a) (expt 2 (1- q))))
	   (<= (+ 1 (* 2 a)) (expt 2 q)))
:hints (("Goal" :do-not-induct t
	 :use ((:instance len=>expt<-aux1-3)))))



(defthm len=>expt<-aux2
  (implies (and (natp q)
		(> q 1)
		(natp a)
		(<= (+ 1 a) (expt 2 (1- q))))
	   (<= (+ 2 (* 2 a)) (expt 2 q)))
:hints (("Goal" :do-not-induct t
	 :use ((:instance len=>expt<-aux1-3)))))



(defthm len=>expt<=
  (implies (and (natp q)
		(> q 1)
		(dgb-p dgop)
		(<= (len dgop) q))
	   (<= (dgb->dgn dgop) (- (expt 2 q) 1)))
  :hints (("Goal" :induct (len=>expt<-schema dgop q))))


(defthm len=>expt<=2
  (implies (and (natp q)
		(= q 1)
		(dgb-p dgop)
		(<= (len dgop) q))
	   (<= (dgb->dgn dgop) (- (expt 2 q) 1)))
  )

(defthm len=>expt<=3
  (implies (and (natp q)
		(= q 0)
		(dgb-p dgop)
		(<= (len dgop) q))
	   (<= (dgb->dgn dgop) (- (expt 2 q) 1)))
  )

(defthm len=>expt<-
  (implies (and (natp q)
		(dgb-p dgop)
		(<= (len dgop) q))
	   (<= (dgb->dgn dgop) (- (expt 2 q) 1)))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance len=>expt<=)
		 (:instance len=>expt<=2)
		 (:instance len=>expt<=3)
	   ))))
